package verifier;

import dk.brics.automaton.State;
import model.DeltaForwardingGraph;
import model.LabeledEdge;
import network.Device;
import util.Logger;

import java.util.*;

public class Verifier {
    private DeltaForwardingGraph dfg;
    private HashSet<Property> properties;

    /**
     * A Verifier verifies a delta forwarding graph with an optional set of policies
     * and two default invariants: loop-free and blackhole-free.
     *
     * @param dfg the delta forwarding graph due the update
     * @param properties policies specified by operator
     */
    public Verifier(DeltaForwardingGraph dfg, HashSet<Property> properties) {
        this.dfg = dfg;
        this.properties = properties;
    }

    public void checkInvariants() {
        for (Device device : this.dfg.graph.vertexSet()) {
            if (device.getName() == "default") {
                continue;
            }
            HashSet<Integer> pset = (HashSet<Integer>) this.dfg.transferredPreds.clone();
            LinkedList<Device> history = new LinkedList<>();
            this.traverse(device, pset, history);
        }
    }

    /**
     * A traverse is a DFS function. During the traverse, it (1) detects loop; (2) detect blackhole.
     * For a device s, it enumerates all possible edge and traversing them with subsets of pset
     * taking intersection with the set of predicates labeled on each edge.
     *
     * @param s the current location (as device)
     * @param pset the set of predicates reaching s
     * @param history the set of devices traversed before.
     */
    private void traverse(Device s, HashSet<Integer> pset, LinkedList<Device> history) {
        if (pset.isEmpty()) {
            return;
        }
        if (history.contains(s)) {
            // Logger.addVerificationReports("DFS-based Verifier" , "Loop", s.getName());
            return;
        }
        for (LabeledEdge edge : this.dfg.graph.edgesOf(s)) {
            if (edge.getFrom() == s) {
                if (edge.getTo().getName() == "default") {
                    // Logger.addVerificationReports("DFS-based Verifier" , "Blackhole", s.getName());
                    return;
                }
                HashSet<Integer> npset = (HashSet<Integer>) pset.clone();
                npset.retainAll(edge.getPredicates());
                LinkedList<Device> nhistory = (LinkedList<Device>) history.clone();
                nhistory.add(s);
                this.traverse(edge.getTo(), npset, nhistory);
            }
        }
    }

    public void checkPolicyDummy() {
        for (Property property: this.properties) {
            if (!this.dfg.graph.vertexSet().contains(property.getSource())) { // delta not affect source
                continue;
            }
            HashSet<Integer> pset = (HashSet<Integer>) this.dfg.transferredPreds.clone();
            HashSet<Device> history = new HashSet<>();
            this.traverseReachDummy(property.getSource(), pset, history, property.getAutomata().getInitialState());
        }
    }

    private void traverseReachDummy(Device s, HashSet<Integer> pset, HashSet<Device> history, State currentState) {
        if (history.contains(s)) {
            // Logger.addVerificationReports("DP-based Verifier" , "Loop", s.getName());
            return;
        }

        for (LabeledEdge edge : this.dfg.graph.edgesOf(s)) {
            if (edge.getFrom() == s) {
                if (edge.getTo().getName() == "default") {
                    // Logger.addVerificationReports("DFS-based Verifier" , "Blackhole", s.getName());
                    return;
                }
                HashSet<Integer> npset = (HashSet<Integer>) pset.clone();
                npset.retainAll(edge.getPredicates());
                State nextState = currentState;
                for (char c : s.getName().toCharArray()) {
                    nextState = nextState.step(c);
                }
                if (nextState == null) return;
                HashSet<Device> nhistory = (HashSet<Device>) history.clone();
                nhistory.add(s);
                this.traverseReachDummy(edge.getTo(), npset, nhistory, nextState);
            }
        }
    }

    public void checkPolicyVector() {
        HashMap<Device, ArrayList<State>> sourceToStates = new HashMap<>();
        for (Property property: this.properties) {
            if (this.dfg.graph.vertexSet().contains(property.getSource())) {
                if (!sourceToStates.containsKey(property.getSource())) {
                    sourceToStates.put(property.getSource(), new ArrayList<>());
                }
                ArrayList<State> states = sourceToStates.get(property.getSource());
                states.add(property.getAutomata().getInitialState());
            }
        }
        HashSet<Integer> pset = (HashSet<Integer>) this.dfg.transferredPreds.clone();
        HashSet<Device> history = new HashSet<>();
        for (Map.Entry<Device, ArrayList<State>> entry : sourceToStates.entrySet()) {
            this.traverseReachVector(entry.getKey(), pset, history, entry.getValue());
        }
    }

    private void traverseReachVector(Device s, HashSet<Integer> pset, HashSet<Device> history, ArrayList<State> States) {
        if (pset.isEmpty()) {
            return;
        }
        if (history.contains(s)) {
            // Logger.addVerificationReports("DFS-based Verifier" , "Loop", s.getName());
            return;
        }
        for (LabeledEdge edge : this.dfg.graph.edgesOf(s)) {
            if (edge.getFrom() == s) {
                if (edge.getTo().getName() == "default") {
                    // Logger.addVerificationReports("DFS-based Verifier" , "Blackhole", s.getName());
                    // FIXME: according to the definition, when npset is empty,
                    //  this edge won't be counted as a blackhole
                    return;
                }
                HashSet<Integer> npset = (HashSet<Integer>) pset.clone();
                npset.retainAll(edge.getPredicates());
                HashSet<Device> nhistory = (HashSet<Device>) history.clone();
                nhistory.add(s);
                ArrayList<State> nextStates = new ArrayList<>();
                for(State cur : States) {
                    State next = cur;
                    for (char c : s.getName().toCharArray()) {
                        next = next.step(c);
                    }
                    if (next == null) {
                        return;
                    } else {
                        nextStates.add(next);
                    }
                }
                this.traverseReachVector(edge.getTo(), npset, nhistory, nextStates);
            }
        }
    }
}
